coverage: 67.22% (+0.1%) from 67.092% — fix-issue-615-interpolation-crash into master

Commit 1bf86b8 extends the issue 615 fix from “reject unsupported model assumptions before they crash MCSAT” to “support tuple-valued model assumptions when they can be safely reduced to existing MCSAT decision types.”

The implemented plan was to keep function-valued tuple leaves out of scope, but allow tuples whose recursively flattened leaves are Bool, Int, Real, scalar, or BitVector. The API validation now accepts exactly those tuple types and still rejects tuples containing function, uninterpreted-sort, finite-field, or otherwise unsupported leaves with MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED.

Internally, MCSAT now tuple-blasts tuple assumptions, recursively flattens the corresponding tuple value from the input model, and decides/caches each scalar leaf value instead of trying to convert the aggregate tuple value into a single mcsat_value_t. Model hints use the same flattening path. The interpolation cleanup path was also fixed so errors propagated from internal model refutation do not leave the two interpolation contexts pushed.

The post-development conclusion is that tuple-valued input-model assumptions are now supported for the same scalar leaf types MCSAT already knows how to decide, without adding tuple support to mcsat_value_construct_from_value. Function-valued tuple leaves remain a separate, larger problem as planned.

Verification passed:

• make -s check-api
• make -s MODE=debug check-api
• release/debug test_issue_615_assumption_type
• git diff --check

Code review provided by Windsurf/Opus4.7:

Code review — b53a1406 ("mcsat: support tuple-valued model assumptions")

Summary

This commit closes issue #615 (MCSAT crashes on model assumptions of unsupported types) and goes one step further by promoting TUPLE_TYPE from "rejected" to "fully supported" whenever the recursively flattened tuple leaves are all MCSAT-decidable scalars (Bool, Int, Real, scalar, BitVector). Anything else — uninterpreted-sort, function, finite-field, function-typed tuple leaves — still fails cleanly at the API boundary with the new MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED error code instead of asserting / segfaulting.

Diff against master: 9 files, ~792/47 +/-, the bulk of which is the new test file.

Touched surface:

• API guard and error plumbing (src/api/yices_api.c, src/api/yices_error.c, src/include/yices.h, src/include/yices_types.h, src/frontend/smt2/smt2_commands.c).
• Preprocessor: a new public symbol preprocessor_tuple_blast exposing the tuple-blast pipeline already used internally for assertions.
• MCSAT solver: a parallel assumption_values vector, a tuple-aware decision/hint registration path, and a SCALAR-aware value constructor.
• A new test file tests/api/test_issue_615_assumption_type.c with 13 test cases.

Strengths

• Properly recursive API guard in mcsat_assumption_type_supported at src/api/yices_api.c:2537-2563. Tuple-of-tuple is allowed iff every leaf is one of the five decidable kinds; everything else falls through to default: return false. The check is run in the existing per-term validation loop (:2579-2587) and sets error->term1/type1 so downstream callers can pinpoint the offending term. Doc updates in src/include/yices.h:3373-3375 and :3426-3428 match.

• Error-code design distinguishes "wrong shape" from "wrong type". The previous shape check (VARIABLE_REQUIRED → MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED) is preserved unchanged; the new type check raises MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED, with an explanatory comment at src/api/yices_api.c:9659-9667. That separation is useful for callers and for the SMT2 frontend's pretty-printing.

• Parallel assumption_values vector in the solver. Pre-fix, mcsat_decide_assumption looked up model_get_term_value(mdl, var_term) at decision time, which only works when the assumption variable is a user-visible term that lives in the model. Tuple-blasted leaves are synthetic new_uninterpreted_terms the user has never seen, so that lookup would fail. Carrying the leaf value alongside the leaf variable at registration time (mcsat_add_assumption_leaf at src/mcsat/solver.c:2807-2812) is the correct data shape and keeps mcsat_decide_assumption a pure consumer.

• Lifecycle is symmetric: assumption_values is initialized in mcsat_construct, deleted in mcsat_destruct, reset both in mcsat_clear and at solve_done: in mcsat_solve, and an assert(mcsat->assumption_values.size == 0) at solve start mirrors the longstanding assumption_vars invariant. No init-once/leak/use-after-reset paths visible.

• mcsat_decide_assumption signature is properly narrowed to value_table_t* vtbl rather than a full model_t* (src/mcsat/solver.c:2461). The body really only ever needed the value table, and the single caller in mcsat_solve passes model_get_vtbl(mdl). Minor but correct.

• Shared blast+flatten helper mcsat_collect_tuple_leaves_and_values at src/mcsat/solver.c:2814-2823 factors the common pre-amble out of mcsat_add_tuple_assumption_leaves and mcsat_set_tuple_hint_leaves. The remaining per-caller bodies are short and intentionally different.

• Hint-vs-assumption asymmetry is documented in code. The assumption path runs preprocessor_apply per leaf and re-asserts leaf = leaf_pre (src/mcsat/solver.c:2841-2851); the hint path does not, and the comment at :2884-2886 calls that out:

  Hints are advisory cache entries, not assumption decisions. No preprocessor_apply/equality assertion is needed here: if a leaf was substituted, search can ignore or overwrite the stale cached hint.

  Decision recorded.

• SCALAR embedding documented inline (src/mcsat/solver.c:2160-2175):

  Scalar values are decided by the rational plugin; the scalar constant index is the corresponding integer value.

  This matters because mcsat_value_construct_from_value only handles BOOLEAN/RATIONAL/ALGEBRAIC/FINITEFIELD/BITVECTOR; SCALAR values would otherwise fall through to its assert(false) arm. The wrapper mcsat_value_construct_from_typed_model_value does the SCALAR conversion explicitly and delegates everything else.

• Interpolation cleanup is now correct on error. yices_check_context_with_interpolation (src/api/yices_api.c:9959-9982) always pops both pushed contexts, even when popping ctx_B fails, and saves+restores the original error report so an inner error code (e.g. MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED raised mid-loop) survives the cleanup. Strict improvement: pre-fix the contexts could be left unbalanced on error and the inner error code was not stable across pop failures.

• Defensive failure paths are annotated. Both tuple registrations longjmp on a malformed user model, with a one-line comment

  Defensive path for malformed user models: API validation has already rejected unsupported tuple leaf types before solver entry.

  pinning the actual trigger (the user gave us a model whose value for the tuple is the wrong shape, or absent).

• preprocessor_tuple_blast docstring spells out the contract at src/mcsat/preprocessor.h:111-117: out is reset by the callee, leaf order matches type_collect_blasted_atom_types, leaves are memoized and stable across later calls. The implementation in src/mcsat/preprocessor.c ivector_reset(out)s explicitly even though tuple_blast_get already resets, which makes the public contract self-evident at the entry point (belt-and-suspenders, harmless).

Concerns

Minor

1. mcsat_collect_tuple_leaves_and_values collapses two failure modes into one bool. The helper returns false for either mcsat_flatten_model_value failure or leaves->size != values->size. Both callers treat them identically and longjmp with MCSAT_EXCEPTION_UNSUPPORTED_THEORY. That's fine today, but MCSAT_EXCEPTION_UNSUPPORTED_THEORY is the wrong code for "user model has the wrong shape" — the theory is supported, the input is malformed. If a future change adds API-boundary validation that the model has a value of the right shape for each tuple assumption, this longjmp becomes genuinely unreachable and either the helper can be simplified (returning void plus assert) or the failure code can be specialized. Not blocking.

2. mcsat_collect_tuple_leaves_and_values expects the out-param ivectors to be empty at entry. The post-condition leaves->size == values->size is only meaningful relative to the in-bound state. Both current callers init immediately before the call so the assumption holds, but if a third caller ever appears a one-line assert(leaves->size == 0 && values->size == 0) at entry would be cheap insurance.

3. mcsat_add_tuple_assumption_leaves runs preprocessor_apply per leaf (src/mcsat/solver.c:2843), which is the right call for soundness when a leaf has been substituted by an earlier assertion. But the loop calls preprocessor_apply even for leaves that have never been touched — every call hits the preprocess_map hash and the preprocess_map is shared across all assertions. For a tuple of arity k with n assumption variables this is O(n·k) hash lookups per solve. Not a problem in practice (k is small), but if you ever have wide tuples it might be cheap to skip the call when the leaf was minted in this solve and could not have been substituted. Optional.

4. build_value_from_flat and merge_blasted_function_value in the preprocessor (called indirectly via preprocessor_build_tuple_model) depend on mcsat_flatten_model_value's recursion order matching type_collect_flat's. That invariant is currently true by construction but is enforced only by the tests. A doc comment on mcsat_flatten_model_value ("recursion order MUST match type_collect_flat") would harden this against future drift. Not blocking.

Test coverage

tests/api/test_issue_615_assumption_type.c runs a focused suite under yices_has_mcsat():

Rejection paths

• check_uninterpreted_sort_assumption_rejected — uninterpreted-sort assumption variables, both _with_model and _with_model_and_hint. Reproduces the original issue Yices crashes during interpolation #615 crash trace.
• check_function_type_assumption_rejected — function-typed assumption variable.
• check_tuple_with_unsupported_leaf_rejected — three tuple-of-{uninterp, function, FF} variants, each must produce MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED.
• check_term_shape_check_preserved — non-uninterpreted assumption term still yields the older MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED (regression guard for the shape vs. type distinction).

Supported scalar paths

• check_supported_types_still_work — Real and SCALAR(3) assumption variables both reach YICES_STATUS_SAT/UNKNOWN. The SCALAR sub-case actually exercises the new mcsat_value_construct_from_typed_model_value SCALAR arm.

Supported tuple paths

• check_tuple_assumption_sat, check_tuple_assumption_unsat, check_nested_tuple_assumption_sat — flat and nested tuples, model-consistent and model-inconsistent.
• check_tuple_with_scalar_leaf — cross-product (int, scalar(3)) exercising both the tuple-flatten path and the SCALAR-via-rational construction together.
• check_tuple_assumption_respects_preprocessing — asserts x = (2, true) and then runs _with_model with the model fixing x to (3, true), expecting UNSAT. Targeted regression for the per-leaf preprocessor_apply call: without it, leaf-level substitution would hide the contradiction.
• check_tuple_repeat_solve_resets_assumptions — calls _with_model twice on the same context with a tuple assumption. Pins the assumption_values reset between solves; without the reset, the assert(mcsat->assumption_values.size == 0) at solve start would fire on the second call.
• check_tuple_model_hint — tuple-typed hint via _with_model_and_hint.
• check_tuple_interpolation_refutation — tuple-typed assumption inside yices_check_context_with_interpolation, exercises the cleanup path on the UNSAT branch.

Coverage assessment

The suite is well-targeted: each non-trivial code path in the diff has at least one test that would fail if that path regressed. The two paths I'd still call slightly under-covered are:

• the longjmp arm in mcsat_collect_tuple_leaves_and_values: there is no test that calls _with_model with a tuple assumption variable but a model that omits or shape-mismatches that variable. A "user supplies an empty model for a tuple assumption" test would either prove the longjmp fires cleanly or motivate moving the check to the API boundary (concern UF problem crashing in symetry breaking #1 above).
• interpolation error preservation: check_tuple_interpolation_refutation covers the success path; there is no test that surfaces an internal error (e.g. unsupported type) through yices_check_context_with_interpolation and asserts the error code survives the cleanup pops. The preservation logic at src/api/yices_api.c:9959-9982 is untested.

Neither gap is a merge-blocker.

Verdict

LGTM. The design is sound, the lifecycle accounting is symmetric, the hint/assumption asymmetry is intentional and called out, the SCALAR sub-fix is documented and tested, and the test suite covers each non-trivial new code path.

The remaining items (helper-failure-mode granularity, redundant preprocessor_apply calls on virgin leaves, doc comments on flatten ordering, the two coverage gaps) are all follow-up tier — none of them block the merge.

Update on the coverage assessment after 2139806:

Both gaps I'd flagged are now closed.

• mcsat_collect_tuple_leaves_and_values longjmp / "model omits the tuple assumption" path — covered by check_tuple_empty_model_uses_default_value in tests/api/test_issue_615_assumption_type.c. It hands yices_check_context_with_model an empty model_t together with a tuple-typed assumption variable, and asserts the call returns cleanly (SAT or UNKNOWN, no YICES_NO_ERROR violation). That exercises the "tuple leaves are unmapped, fall through to defaults" branch end-to-end without going through the longjmp.
• Interpolation error preservation across the cleanup pops — covered by check_interpolation_preserves_refutation_error. ctx_A is mcsat-with-interpolation, ctx_B is a default context asserting an inequality over an uninterpreted-sort variable. The internal model refutation in ctx_A then runs _with_model over an unsupported assumption type, raising MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED. The test asserts that this error code survives the cleanup-pops in yices_check_context_with_interpolation (src/api/yices_api.c:9959-9982). That's the exact preservation path I called untested.

With these in, every non-trivial branch in the diff has at least one regression test that would fail if it regressed. No remaining coverage concerns from my side.